Nuprl Definition : es-dstate-when
11,40
postcript
pdf
(discrete state when
e
)(
x
) == if discrete(loc(
e
);
x
) then
x
when
e
else
fi
latex
clarification:
es-dstate-when(
es
;
e
)(
x
) == if es-isconst(
es
;es-loc(
es
;
e
);
x
) then es-when(
es
;
x
;
e
) else
fi
latex
Definitions
x
.
A
(
x
)
,
if
b
then
t
else
f
fi
,
discrete(
i
;
x
)
,
loc(
e
)
,
x
when
e
,
FDL editor aliases
es-dstate-when
origin
fi
fi fi
fi 
x.A(x)